grammar RealSetConstruction;

options {
  language=Java;
  output = AST;
  ASTLabelType=CommonTree;
  k=9;  
}

 
tokens {      
  LCURLY = '{';  
  NEWLINE = '\n';
  FORALL = 'forall';
  EXISTS = 'exists';
  NOT = 'not';
 }

@header {
 package real;
  
 import real.lang.*;
 import real.evaluation.*;
 import real.evaluation.set.*;
 import real.evaluation.formula.*;
}

@lexer::header {
 package real;
}
 

/*tuple :
   '(' ID (',' ID )+ ')' */ 
   /* translate all tuples to special free id */   
  //;

setConstruction returns [RealSetConstruction result]
  : items+=element ( ',' items+=element  )*
  { 
    RealSetConstruction res = new RealSetConstruction();
    List<SyntacticalConstruction<? extends RealObject>> list = new ArrayList<SyntacticalConstruction<? extends RealObject>>();     
    for (int i = 0; i < $items.size(); i++) {
      element_return element = (element_return) $items.get(i); 
      list.add(element.item);
    }
    res.setElements(list);
    $result = res;
  }  
  | ID SUCH_THAT phi=formula 
  {          
    $result = new ConstrainedSetConstruction($ID.text, $phi.formula);
  } 
  | inset SUCH_THAT phi=formula
  { 
    /*RealSetConstruction res = RealSetConstruction.CONSTRAINTED_ELEMENT;
    res.setFormula($phi.formula);
    $result = res;*/
  }  
  ;

element returns[SyntacticalConstruction item]
  : ID {$item = new SymbolConstruction($ID.text);} 
  ;

formula returns [Formula formula]
  : rho=compositeFormulaExpr {$formula = $rho.formula;}
  ;

compositeFormulaExpr  returns [Formula formula]
  : or=orFormula { $formula = $or.formula; }
  | q=quatifiedFormula  { $formula = $q.formula; }
  ;

quatifiedFormula returns [Formula formula]
  : FORALL inset '.' compositeFormulaExpr 
  | EXISTS inset '.' compositeFormulaExpr
  ;

orFormula returns [CompositeFormulaExpression formula]
  : items+=andFormula (OR items+=andFormula)* 
  {
    List<CompositeFormulaExpression> formulas = new ArrayList<CompositeFormulaExpression>();     
    for (int i = 0; i < $items.size(); i++) {
      andFormula_return phi = (andFormula_return) $items.get(i); 
      formulas.add(phi.formula);
    }
    $formula = new CompositeFormulaExpression(LogicalJunction.OR, formulas);
  }
  ;

andFormula returns [CompositeFormulaExpression formula]
  : items+=notFormula (AND items+=notFormula)*
  {
    List<Formula> formulas = new ArrayList<Formula>();     
    for (int i = 0; i < $items.size(); i++) {
      notFormula_return rho = (notFormula_return) $items.get(i); 
      formulas.add(rho.formula);
    }
    $formula = new CompositeFormulaExpression(LogicalJunction.AND, formulas);
  }
  ;

notFormula returns [Formula formula]
  : a=atomicFormula { $formula = $a.formula;} 
  | (NOT na=atomicFormula) { $formula = new CompositeFormulaExpression(LogicalJunction.NOT, $na.formula); } 
  ;

/* An important feature of REAL language is that there is no way to determine
whether a fixed formula expression is a predicate (no free variables). To support a rich
and nonrestricted formalism this fact can be decided only on evaluation step */
atomicFormula returns [Formula formula]
  : inset 
  | subset 
  | superset 
  // TODO: refer predicate symbols names, <, >, = other predicates
  | '(' ! compositeFormulaExpr ')' !
  ;

inset  : ID 'is'?  'in' ID;

not_inset  : ID 'is'? NOT 'in' ID;

subset  : ID 'is'? 'a'? 'subset' 'of'? ID;

superset : ID 'is'? 'a'? 'superset' 'of'? ID;

RCURLY 
  : '}'
  /* Here we should emit EOF token, and finish contruction */ 
  ;

ID    :   ('_'|'a'..'z'|'A'..'Z') ('_'|'a'..'z'|'A'..'Z'|'0'..'9')* ;

SUCH_THAT : ('|' | ':' | 's.t.' | (',' 's.t.') |  (',' 'such' 'that'));

OR  : 'or' | '\\/';

AND : 'and' | '/\\' | ';'; 
  
WS    :   (' '|'\t')+      {$channel=HIDDEN;} ;
CMT   :   '/*' .* '*/'     {$channel=HIDDEN;} ;